sv:(Id(T:Type  (T + (T)))), av:(KndType), dis:(IdId),
cl:(Id(n:  base-domain-type(n))Realizer), fr, rfr:(IdId(Knd List)),
sfr:(IdLnkId(Knd List)), afr:(IdKnd((Id List) + Top)), bfr:(IdKnd((IdLnk List) + Top)).
(k:Knd. av(k))
 (R:Realizer.
 R-FeasibleWitness{i:l}(R; sv; av; dis; cl; fr; sfr; rfr; afr; bfr)  R-Feasible(R)) 

latex

Definitions

A c B, , Normal(T), True, Normal(ds), xdom(f). v=f(x)   P(x;v), t.2, t.1, P & Q, x. t(x), t  T, R-Feasible(R), R-FeasibleWitness, P  Q, Top, x:A. B(x), x(s), Unit, Realizer, S  T, left  right, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), Rnone(),

Lemmas

R-FeasibleWitness-compat, base-domain-type wf, Id wf, top wf, Knd wf, es realizer wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, id-deq wf, fpf-ap wf, Rsframe wf, Rframe wf, int inc rationals, pi2 wf, Rinit wf, Rplus wf, R-Feasible-Rplus, Rnone wf, R-FeasibleWitness wf, bool wf, finite-prob-space wf, IdLnk wf, decl-type wf, decl-state wf, fpf wf, rationals wf, unit wf